Current Result Document :
| 한글제목(Korean Title) |
모나딕 타입으로 Coq에서 배중률 사용을 안전하게 감싸기 |
| 영문제목(English Title) |
Safe Encapsulation of using LEM in Coq by Monadic Type |
| 저자(Author) |
Jihee Park
Sukyoung Ryu
박지희
류석영
|
| 원문수록처(Citation) |
VOL 49 NO. 02 PP. 1236 ~ 1238 (2022. 12) |
한글내용
(Korean Abstract) |
증명을 위한 프로그래밍 언어인 Coq은 구성 논리 체계를 가지고 있어, 수학자들이 일반적으로 따르는 배중률이 기본 법칙도 아니고 유도되는 정리도 아니다. 배중률을 Coq에 추가하기 위해 주로 공리를 추가하는데, 이러한 경우 배중률 공리를 사용하여 증명한 명제와 그렇지 않은 명제를 구분할 수 없는 문제가 있다. 이 연구에서는 모나딕 타입을 이용해 배중률 공리를 사용하여 증명한 명제를 타입으로 구분하면서도 Coq tactic을 제공해 쉬운 증명을 가능하게 한다. 추가로 배중률을 가정하여 증명한 귀납적 모나딕 타입과 이중 부정 타입을 정의하여 세 가지 타입이 논리적으로 동치 관계에 있음을 증명한다. |
영문내용
(English Abstract) |
|
| 키워드(Keyword) |
|
| 파일첨부 |
PDF 다운로드
|
